Search for: All records

Cyber-physical systems (CPS) designed in simulators, often consisting of multiple interacting agents (e.g., in multi-agent formations), behave differently in the real-world. We would like to verify these systems during runtime when they are deployed. Thus, we propose robust predictive runtime verification (RPRV) algorithms for: (1) general stochastic CPS under signal temporal logic (STL) tasks, and (2) stochastic multi-agent systems (MAS) under spatio-temporal logic tasks. The RPRV problem presents the following challenges: (1) there may not be sufficient data on the behavior of the deployed CPS, (2) predictive models based on design phase system trajectories may encounter distribution shift during real-world deployment, and (3) the algorithms need to scale to the complexity of MAS and be applicable to spatio-temporal logic tasks. To address these challenges, we assume knowledge of an upper bound on the statistical distance (in terms of anf-divergence) between the trajectory distributions of the system at deployment and design time. We are motivated by our prior work where we proposed an accurate and an interpretable RPRV algorithm for general CPS, which we here extend to the MAS setting and spatio-temporal logic tasks. Specifically, we use a learned predictive model to estimate the system behavior at runtime androbust conformal predictionto obtain probabilistic guarantees by accounting for distribution shifts. Building on our prior work, we perform robust conformal prediction over the robust semantics of spatio-temporal reach and escape logic (STREL) to obtain centralized RPRV algorithms for MAS. We empirically validate our results in a drone swarm simulator, where we show the scalability of our RPRV algorithms to MAS and analyze the impact of different trajectory predictors on the verification result. To the best of our knowledge, these are the first statistically valid algorithms for MAS under distribution shift. 

Abstract Over the past decade, magnetoelectric nanoparticles (MENPs) have proven effective in generating local electric fields in response to stimulation with a magnetic field. The applications of such nanoparticles are many and varied, with examples of prior research including use for on-demand drug release, wireless modulation and recording of neural activity, and organic dye degradation. This study investigates the potential for organic dye degradation to be used as a rapid and efficient screening tool to detect the magnetoelectric effect of MENPs, and how the results of such a test mirror the antiproliferative effect of said nanoparticles. Trypan blue was selected as an azo dye to test for dye degradation. Vials of the dye were treated with CoFe2O4@BaTiO3 core-shell MENPs of varying characteristics, both with and without concurrent 1-kHz 250-Oe magnetic stimulation. Dye degradation was measured using ultraviolet (UV)-vis spectroscopy. Dye degradation efficacy varied with varying nanoparticle synthesis parameters. As controls, nanoparticles of the same composition, but with an insignificant magnetoelectric effect, were used. SKOV-3 ovarian cancer cells were then treated with the same nanoparticles, and viability was measured with an adenosine triphosphate (ATP) assay. These measurements show a decrease in cell viability up to 60.3% of control (p = 0.0052), which mirrored the efficacy of dye degradation of up to 69.8% (p = 0.0037) in each of the particle variants, demonstrating the value of azo dye degradation as a simple screening test for MENPs, and showing the potential of MENPs used as wirelessly controlled nanodevices to allow targeted electric field-based treatments. 

We show that there is an absolute constant c > 0 c>0 such that the following holds. For every n > 1 n > 1 , there is a 5-uniform hypergraph on at least 2 2 c n 1 / 4 2^{2^{cn^{1/4}}} vertices with independence number at most n n , where every set of 6 vertices induces at most 3 edges. The double exponential growth rate for the number of vertices is sharp. By applying a stepping-up lemma established by the first two authors, analogous sharp results are proved for k k -uniform hypergraphs. This answers the penultimate open case of a conjecture in Ramsey theory posed by Erdős and Hajnal in 1972.